r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a).
(
w:|r|. SqStable(a(w)))
(u, v:|r|. ([u]{|r / d|} = [v]{|r / d|} 
|r / d|) 
(a(u +r (-r(v))))) | 13,42 |
r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a).
w:|r|. SqStable(a(w)))
(u, v:|r|. ([u]{|r / d|} = [v]{|r / d|} |r / d|) (a(u +r (-r(v)))))
| Up | |
| Definitions | |
| Lemmas |